Nuprl Definition : ma-single-pre-init 0,22
with ds: ds init: initaction a:T precondition a(v) is P
== mk-ma(ds;
== locl(a) : T;
== init;
== a : P;
== ;
== ;
== ;
== ;
== ;
== ;
== ) 
latex

Definitionsmk-ma, locl(a), x : v,
FDL editor aliasesma-single-pre-init

origin